{
 "cells": [
  {
   "cell_type": "markdown",
   "id": "665edd84-1608-4a8b-8fe0-fde3a2c1d776",
   "metadata": {},
   "source": [
    "# IMO 2024 -- LeanDojo"
   ]
  },
  {
   "cell_type": "markdown",
   "id": "ab9cc32b-45e3-42c3-b701-6218f77ce429",
   "metadata": {},
   "source": [
    "Setup the environment variable `GITHUB_ACCESS_TOKEN` to avoid rate limiting.\n",
    "\n",
    "```bash\n",
    "GITHUB_ACCESS_TOKEN=...\n",
    "```"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 1,
   "id": "12b0b8b0-76e6-47d4-ae28-a70d48b3b619",
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/plain": [
       "True"
      ]
     },
     "execution_count": 1,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    "from dotenv import load_dotenv\n",
    "# set GITHUB_ACCESS_TOKEN\n",
    "load_dotenv(override=True)"
   ]
  },
  {
   "cell_type": "markdown",
   "id": "c3ec1660",
   "metadata": {},
   "source": [
    "## Lean Git Repository"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 2,
   "id": "34e0a2b3-69f7-4d33-a648-4e7362135ade",
   "metadata": {},
   "outputs": [
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "2.1.2\n"
     ]
    }
   ],
   "source": [
    "from lean_dojo import LeanGitRepo, trace, Dojo, Theorem\n",
    "import lean_dojo\n",
    "print(lean_dojo.__version__)"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 3,
   "id": "c18248f8-e4f8-4123-a810-9aac0f54f20e",
   "metadata": {},
   "outputs": [
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "fatal: destination path 'IMO_2024' already exists and is not an empty directory.\n"
     ]
    }
   ],
   "source": [
    "!git clone https://github.com/Lean-zh/IMO_2024"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 4,
   "id": "761ab76b-c66c-4011-914f-ebfc367639da",
   "metadata": {},
   "outputs": [
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "basic.py  \u001b[0m\u001b[01;34mIMO_2024\u001b[0m/  leandojo.ipynb  p3.ipynb\n"
     ]
    }
   ],
   "source": [
    "ls ."
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 5,
   "id": "7218d328-0608-4a81-aa7d-47f1346de5a0",
   "metadata": {},
   "outputs": [],
   "source": [
    "repo = LeanGitRepo('IMO_2024', 'main')"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 6,
   "id": "7c15a65b",
   "metadata": {},
   "outputs": [
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "repo.url /home/cuber/LeanPorjects/IMO_Resource/scripts/IMO_2024\n",
      "repo.commit c3e025a8a525b5a12f105e8c39d188adb8bab24b\n",
      "repo.lean_version v4.10.0-rc2\n",
      "repo.name IMO_2024\n",
      "repo.commit_url /home/cuber/LeanPorjects/IMO_Resource/scripts/IMO_2024/tree/c3e025a8a525b5a12f105e8c39d188adb8bab24b\n",
      "{'content': 'leanprover/lean4:v4.10.0-rc2\\n'}\n"
     ]
    }
   ],
   "source": [
    "print(\"repo.url\", repo.url)\n",
    "print(\"repo.commit\", repo.commit)\n",
    "print(\"repo.lean_version\", repo.lean_version)\n",
    "print(\"repo.name\", repo.name)\n",
    "print(\"repo.commit_url\", repo.commit_url)\n",
    "print(repo.get_config(\"lean-toolchain\"))"
   ]
  },
  {
   "cell_type": "markdown",
   "id": "70f868f5",
   "metadata": {},
   "source": [
    "## Trace Lean Repo"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "id": "3579d930",
   "metadata": {
    "collapsed": true,
    "jupyter": {
     "outputs_hidden": true
    },
    "scrolled": true
   },
   "outputs": [],
   "source": [
    "# this takes long time\n",
    "traced_repo = trace(repo)"
   ]
  },
  {
   "cell_type": "markdown",
   "id": "3cfbfa69-f306-4fbc-83b0-a9ed3ecb4ccf",
   "metadata": {},
   "source": [
    "## Interaction "
   ]
  },
  {
   "cell_type": "markdown",
   "id": "6b101ad8-8b49-456d-aeb9-183b6e4be41f",
   "metadata": {},
   "source": [
    "### p1"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 8,
   "id": "461a853b-b2f9-412e-b25c-b0453f4ceb54",
   "metadata": {},
   "outputs": [],
   "source": [
    "from lean_dojo import Theorem, Dojo"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 11,
   "id": "4d341648-1921-4d7c-ab85-0200c194e620",
   "metadata": {},
   "outputs": [],
   "source": [
    "theorem = Theorem(repo, \"IMO2024/p1.lean\", \"imo_2024_p1\")"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 14,
   "id": "a3599478-7528-4182-8e7d-5d40d944e2f6",
   "metadata": {},
   "outputs": [
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "⊢ {α | ∀ (n : ℕ), 0 < n → ↑n ∣ ∑ i ∈ Finset.Icc 1 n, ⌊↑i * α⌋} = {α | ∃ k, Even k ∧ α = ↑k}\n"
     ]
    }
   ],
   "source": [
    "dojo, state_0 = Dojo(theorem).__enter__()\n",
    "print(state_0.pp)"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 15,
   "id": "e5952e8a-39b4-4b74-ae5a-96396210de01",
   "metadata": {},
   "outputs": [
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "⊢ {α | ∀ (n : ℕ), 0 < n → ↑n ∣ ∑ i ∈ Finset.Icc 1 n, ⌊↑i * α⌋} ⊆ {α | ∃ k, Even k ∧ α = ↑k} ∧\n",
      "    {α | ∃ k, Even k ∧ α = ↑k} ⊆ {α | ∀ (n : ℕ), 0 < n → ↑n ∣ ∑ i ∈ Finset.Icc 1 n, ⌊↑i * α⌋}\n"
     ]
    }
   ],
   "source": [
    "state_1 = dojo.run_tac(state_0, \"rw [Set.Subset.antisymm_iff]\")\n",
    "print(state_1.pp)"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 17,
   "id": "d89db3aa-13f3-4d03-a047-c28299ec5114",
   "metadata": {},
   "outputs": [
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "⊢ (∀ x ∈ {α | ∀ (n : ℕ), 0 < n → ↑n ∣ ∑ i ∈ Finset.Icc 1 n, ⌊↑i * α⌋}, x ∈ {α | ∃ k, Even k ∧ α = ↑k}) ∧\n",
      "    {α | ∃ k, Even k ∧ α = ↑k} ⊆ {α | ∀ (n : ℕ), 0 < n → ↑n ∣ ∑ i ∈ Finset.Icc 1 n, ⌊↑i * α⌋}\n"
     ]
    }
   ],
   "source": [
    "state_2 = dojo.run_tac(state_1, \"rw [Set.subset_def]\")\n",
    "print(state_2.pp)"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 18,
   "id": "a598c8cc-d82c-468f-8fa3-fdbece084456",
   "metadata": {},
   "outputs": [],
   "source": [
    "state_3 = dojo.run_tac(state_2, \"exists λx L=>(L 2 two_pos).rec λl Y=>?_\")"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 31,
   "id": "2b647eb2-646b-4ac4-9d57-b3d74354bd63",
   "metadata": {},
   "outputs": [
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "2\n",
      "case refine_1\n",
      "⊢ {α | ∃ k, Even k ∧ α = ↑k} ⊆ {α | ∀ (n : ℕ), 0 < n → ↑n ∣ ∑ i ∈ Finset.Icc 1 n, ⌊↑i * α⌋}\n",
      "\n",
      "case refine_2\n",
      "x : ℝ\n",
      "L : x ∈ {α | ∀ (n : ℕ), 0 < n → ↑n ∣ ∑ i ∈ Finset.Icc 1 n, ⌊↑i * α⌋}\n",
      "l : ℤ\n",
      "Y : ∑ i ∈ Finset.Icc 1 2, ⌊↑i * x⌋ = ↑2 * l\n",
      "⊢ x ∈ {α | ∃ k, Even k ∧ α = ↑k}\n"
     ]
    }
   ],
   "source": [
    "print(len(state_3.goals))\n",
    "print(state_3.pp)"
   ]
  },
  {
   "cell_type": "markdown",
   "id": "b413c113-8fcd-4c53-aa47-f7dda355b457",
   "metadata": {},
   "source": [
    "### p2"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 28,
   "id": "0ac6d867-24e2-4620-99b4-dd28336fef45",
   "metadata": {},
   "outputs": [],
   "source": [
    "theorem = Theorem(repo, \"IMO2024/p2.lean\", \"imo_2024_p2\")"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 29,
   "id": "9afd37c1-6867-44f1-bcf9-70f9d0b11302",
   "metadata": {},
   "outputs": [
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "⊢ {(a, b) | 0 < a ∧ 0 < b ∧ ∃ g N, 0 < g ∧ 0 < N ∧ ∀ n ≥ N, (a ^ n + b).gcd (b ^ n + a) = g} = {(1, 1)}\n"
     ]
    }
   ],
   "source": [
    "dojo, state_0 = Dojo(theorem).__enter__()\n",
    "print(state_0.pp)"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 30,
   "id": "74d60bd1-42c0-4c66-b5fc-dbb8b13eabb4",
   "metadata": {},
   "outputs": [
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "case zero\n",
      "⊢ {(a, b) | 0 < a ∧ 0 < b ∧ ∃ g N, 0 < g ∧ 0 < N ∧ ∀ n ≥ N, (a ^ n + b).gcd (b ^ n + a) = g} = {(1, 1)}\n",
      "\n",
      "case succ\n",
      "n✝ : ℕ\n",
      "a✝ : {(a, b) | 0 < a ∧ 0 < b ∧ ∃ g N, 0 < g ∧ 0 < N ∧ ∀ n ≥ N, (a ^ n + b).gcd (b ^ n + a) = g} = {(1, 1)}\n",
      "⊢ {(a, b) | 0 < a ∧ 0 < b ∧ ∃ g N, 0 < g ∧ 0 < N ∧ ∀ n ≥ N, (a ^ n + b).gcd (b ^ n + a) = g} = {(1, 1)}\n"
     ]
    }
   ],
   "source": [
    "state_1 = dojo.run_tac(state_0, \"induction(10)+2\")\n",
    "print(state_1.pp)"
   ]
  },
  {
   "cell_type": "markdown",
   "id": "0ab6a3b4-f492-4ce0-b3d4-8ecd02a481ed",
   "metadata": {},
   "source": [
    "### p6"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 32,
   "id": "c59fee24-959a-4f5c-8c01-650f8285d2df",
   "metadata": {},
   "outputs": [],
   "source": [
    "theorem = Theorem(repo, \"IMO2024/p6.lean\", \"imo_2024_p6\")"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 33,
   "id": "8ecabab2-ba28-43d1-9f61-5f06c06b07f1",
   "metadata": {},
   "outputs": [
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "IsAquaesulian : (ℚ → ℚ) → Prop\n",
      "IsAquaesulian_def : ∀ (f : ℚ → ℚ), IsAquaesulian f ↔ ∀ (x y : ℚ), f (x + f y) = f x + y ∨ f (f x + y) = x + f y\n",
      "⊢ IsLeast\n",
      "    {c | ∀ (f : ℚ → ℚ), IsAquaesulian f → {x | ∃ r, f r + f (-r) = x}.Finite ∧ ↑{x | ∃ r, f r + f (-r) = x}.ncard ≤ c} 2\n"
     ]
    }
   ],
   "source": [
    "dojo, state_0 = Dojo(theorem).__enter__()\n",
    "print(state_0.pp)"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 34,
   "id": "26a82706-d44c-4ec6-b283-6e3e0209dac1",
   "metadata": {},
   "outputs": [
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "case refine_1\n",
      "IsAquaesulian : (ℚ → ℚ) → Prop\n",
      "IsAquaesulian_def : ∀ (f : ℚ → ℚ), IsAquaesulian f ↔ ∀ (x y : ℚ), f (x + f y) = f x + y ∨ f (f x + y) = x + f y\n",
      "⊢ 2 ∈ {c | ∀ (f : ℚ → ℚ), IsAquaesulian f → {x | ∃ r, f r + f (-r) = x}.Finite ∧ ↑{x | ∃ r, f r + f (-r) = x}.ncard ≤ c}\n",
      "\n",
      "case refine_2\n",
      "IsAquaesulian : (ℚ → ℚ) → Prop\n",
      "IsAquaesulian_def : ∀ (f : ℚ → ℚ), IsAquaesulian f ↔ ∀ (x y : ℚ), f (x + f y) = f x + y ∨ f (f x + y) = x + f y\n",
      "⊢ 2 ∈\n",
      "    lowerBounds\n",
      "      {c | ∀ (f : ℚ → ℚ), IsAquaesulian f → {x | ∃ r, f r + f (-r) = x}.Finite ∧ ↑{x | ∃ r, f r + f (-r) = x}.ncard ≤ c}\n"
     ]
    }
   ],
   "source": [
    "state_1 = dojo.run_tac(state_0, \"exists@?_\")\n",
    "print(state_1.pp)"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "id": "ba73036d-a415-4296-9297-29b7afea5a8d",
   "metadata": {},
   "outputs": [],
   "source": []
  }
 ],
 "metadata": {
  "kernelspec": {
   "display_name": "Python 3",
   "language": "python",
   "name": "python3"
  },
  "language_info": {
   "codemirror_mode": {
    "name": "ipython",
    "version": 3
   },
   "file_extension": ".py",
   "mimetype": "text/x-python",
   "name": "python",
   "nbconvert_exporter": "python",
   "pygments_lexer": "ipython3",
   "version": "3.10.14"
  }
 },
 "nbformat": 4,
 "nbformat_minor": 5
}
